In the context of large language models (LLMs), current advanced reasoning methods have made impressive strides in various reasoning tasks. However, when it comes to logical reasoning tasks, major challenges remain in both efficacy and efficiency. This is rooted in the fact that these systems fail to fully leverage the inherent structure of logical tasks throughout the reasoning processes such as decomposition, search, and resolution. To address this, we propose a logic-complete reasoning framework, Aristotle, with three key components: Logical Decomposer, Logical Search Router, and Logical Resolver. In our framework, symbolic expressions and logical rules are comprehensively integrated into the entire reasoning process, significantly alleviating the bottlenecks of logical reasoning, i.e., reducing sub-task complexity, minimizing search errors, and resolving logical contradictions. The experimental results on several datasets demonstrate that Aristotle consistently outperforms state-of-the-art reasoning frameworks in both accuracy and efficiency, particularly excelling in complex logical reasoning scenarios. We will open-source all our code at https://github.com/Aiden0526/Aristotle.

Numerous neuro-symbolic approaches have recently been proposed typically with the goal of adding symbolic knowledge to the output layer of a neural network. Ideally, such losses maximize the probability that the neural network's predictions satisfy the underlying domain. Unfortunately, this type of probabilistic inference is often computationally infeasible. Neuro-symbolic approaches therefore commonly resort to fuzzy approximations of this probabilistic objective, sacrificing sound probabilistic semantics, or to sampling which is very seldom feasible. We approach the problem by first assuming the constraint decomposes conditioned on the features learned by the network. We iteratively strengthen our approximation, restoring the dependence between the constraints most responsible for degrading the quality of the approximation. This corresponds to computing the mutual information between pairs of constraints conditioned on the network's learned features, and may be construed as a measure of how well aligned the gradients of two distributions are. We show how to compute this efficiently for tractable circuits. We test our approach on three tasks: predicting a minimum-cost path in Warcraft, predicting a minimum-cost perfect matching, and solving Sudoku puzzles, observing that it improves upon the baselines while sidestepping intractability.

As is known, AGI (Artificial General Intelligence), unlike AI, should operate with meanings. And that's what distinguishes it from AI. Any successful AI implementations (playing chess, unmanned driving, face recognition etc.) do not operate with the meanings of the processed objects in any way and do not recognize the meaning. And they don't need to. But for AGI, which emulates human thinking, this ability is crucial. Numerous attempts to define the concept of "meaning" have one very significant drawback - all such definitions are not strict and formalized, so they cannot be programmed. The meaning search procedure should use a formalized description of its existence and possible forms of its perception. For the practical implementation of AGI, it is necessary to develop such "ready-to-code" descriptions in the context of their use for processing the related cognitive concepts of "meaning" and "knowledge". An attempt to formalize the definition of such concepts is made in this article.

Biological data and knowledge bases increasingly rely on Semantic Web technologies and the use of knowledge graphs for data integration, retrieval and federated queries. We propose a solution for automatically semantifying biological assays. Our solution contrasts the problem of automated semantification as labeling versus clustering where the two methods are on opposite ends of the method complexity spectrum. Characteristically modeling our problem, we find the clustering solution significantly outperforms a deep neural network state-of-the-art labeling approach. This novel contribution is based on two factors: 1) a learning objective closely modeled after the data outperforms an alternative approach with sophisticated semantic modeling; 2) automatically semantifying biological assays achieves a high performance F 1 of nearly 83%, which to our knowledge is the first reported standardized evaluation of the task offering a strong benchmark model.

Deduction Theorem: The Problematic Nature of Common Practice in Game Theory Holger I. MEINHARDT † August 2, 2019 We consider the Deduction Theorem that is used in the literature of game theory to run a purported proof by contradiction. In the context of game theory, it is stated that if we have a proof of φ null ϕ, then we also have a proof of φ ϕ. Hence, the proof of φ ϕ is deduced from a previous known statement. However, we argue that one has to manage to prove that the clauses φ and ϕ exist, i.e., they are known true statements in order to establish that φ null ϕ is provable, and that therefore φ ϕ is provable as well. Thus, we are only allowed to reason with known true statements, i.e., we are not allowed to assume that φ or ϕ exist. Doing so, leads immediately to a wrong conclusion. Apart from this, we stress to other facts why the Deduction Theorem is not applicable to run a proof by contradiction. Finally, we present an example from industrial cooperation where the Deduction Theorem is not correctly applied with the consequence that the obtained result contradicts the well-known aggregation issue. MS Classifications 2010: 03B05, 91A12, 91B24 Keywords: Propositional Logic, Deduction Theorem, Herbrand Theorem, Proof by Contradiction, TU Games, Cooperative Oligopoly Games, Partition Function Approach, γ -Belief, Nash Equilibrium, Aggregation across Firms. 1 Introduction We review a common practice in the literature of game theory of applying the Deduction Theorem (Herbrand Theorem, 1930) on a purported proof by contradiction.

We present a novel approach to constraint-based causal discovery, that takes the form of straightforward logical inference, applied to a list of simple, logical statements about causal relations that are derived directly from observed (in)dependencies. It is both sound and complete, in the sense that all invariant features of the corresponding partial ancestral graph (PAG) are identified, even in the presence of latent variables and selection bias. The approach shows that every identifiable causal relation corresponds to one of just two fundamental forms. More importantly, as the basic building blocks of the method do not rely on the detailed (graphical) structure of the corresponding PAG, it opens up a range of new opportunities, including more robust inference, detailed accountability, and application to large models.